COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDVAR x y z s
C00004 ENDMK
C⊗;
declare INDVAR x y z s;

declare INDCONST I, S0, desk, home,car,airport,county;

declare PREDCONST at 3, att 2, walkable 1, drivable 1;

declare OPCONST walk 2, drive 2;

axiom walkable:	walkable(home);;

axiom drivable:	drivable(county);;

axiom at:
	at(I,desk,S0)
	att(desk,home)
	at(car,home,S0)
	att(home,county)
	att(airport,county)
;;

axiom attrans:
	∀x y z s.((att(x,y) ∨ at(x,y,s)) ∧ (att(y,z) ∨ at(y,z,s)) ⊃ at(x,z,s))
	∀x y z.(att(x,y) ∧ att(y,z) ⊃ att(x,z))
;;

axiom walk:
	∀x y z s.((walkable(x) ∧ (att(y,x)∨at(y,x,s)) ∧ (att(z,x)∨at(z,x,s))
			 ∧ at(I,y,s))
		⊃ (at(I,z,walk(z,s))
		   ∧ ∀x y.(¬(x = I) ⊃ (at(x,y,walk(z,s)) ≡ at(x,y,s)))))
;;

axiom drive:
	∀x y z s.((drivable(x) ∧ att(y,x) 
				∧ att(z,x) ∧ at(car,y,s) ∧ at(I,car,s))
		⊃ (at(car,z,drive(z,s))
			∧ ∀x y.(¬(x = car ∨ at(x,car,s)) ∨ y=car
					 ⊃ (at(x,y,drive(z,s)) ≡ at(x,y,s)))))
;;

axiom notI:	¬(I=desk) ∧ ¬(I=car) ∧ ¬(I=home) ∧ ¬(I=airport);;